{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# 假设\n",
    "\n",
    "原文: https://docs.sympy.org/latest/modules/assumptions/assume.html\n",
    "\n",
    "一个实现谓词和假设上下文的模块。\n",
    "\n",
    "## 类 class sympy.assumptions.assume.AppliedPredicate(predicate, *args)\n",
    "\n",
    "由于将 `Predicate` 应用于参数而产生的表达式类。`AppliedPredicate` 仅仅包装它的参数并保持未计算状态。要评估它，请使用 `ask()`函数。\n",
    "\n",
    "### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle Q.integer(1)$"
      ],
      "text/plain": [
       "Q.integer(1)"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import Q, ask\n",
    "Q.integer(1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`Function` 属性返回谓词，`arguments` 属性返回参数的元组。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "<class 'sympy.assumptions.assume.AppliedPredicate'>\n",
      "Q.integer\n",
      "(1,)\n"
     ]
    }
   ],
   "source": [
    "print(type(Q.integer(1)))\n",
    "print(Q.integer(1).function)\n",
    "print(Q.integer(1).arguments)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "应用谓词可以计算到`ask`的布尔值 :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ask(Q.integer(1))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 属性 arg\n",
    "\n",
    "返回该假设使用的表达式。\n",
    "\n",
    "### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle x + 1$"
      ],
      "text/plain": [
       "x + 1"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import Q, Symbol\n",
    "x = Symbol('x')\n",
    "a = Q.integer(x + 1)\n",
    "a.arg"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 属性 arguments\n",
    "\n",
    "返回应用于谓词的参数。\n",
    "\n",
    "### 属性 function\n",
    "\n",
    "返回谓词。\n",
    "\n",
    "## 类 class sympy.assumptions.assume.AssumptionsContext\n",
    "Set containing default assumptions which are applied to the ask() function.\n",
    "\n",
    "设置包含应用于 `ask()`函数的默认假设。\n",
    "\n",
    "### 解释\n",
    "\n",
    "这用于表示全局假设，但也可以使用此类创建自己的局部假设上下文。它基本上是 Python 集合的一个瘦包装器，因此请参阅其高级用法的文档。\n",
    "\n",
    "### 例子\n",
    "\n",
    "默认的假设上下文是 `global_premissions`，最初是空的:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "AssumptionsContext()"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import ask, Q\n",
    "from sympy.assumptions import global_assumptions\n",
    "global_assumptions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "可以添加默认假设:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{Q.real(x)}"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy.abc import x\n",
    "global_assumptions.add(Q.real(x))\n",
    "global_assumptions"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ask(Q.real(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "以及移除默认假设: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "None\n"
     ]
    }
   ],
   "source": [
    "global_assumptions.remove(Q.real(x))\n",
    "print(ask(Q.real(x)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`Clear()`方法消除了所有的假设:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{Q.positive(x)}"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "global_assumptions.add(Q.positive(x))\n",
    "global_assumptions"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "AssumptionsContext()"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "global_assumptions.clear()\n",
    "global_assumptions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    ">参见: 假设\n",
    "\n",
    "### 方法 add(*assumptions)\n",
    "\n",
    "增加假设。\n",
    "\n",
    "## 类 class sympy.assumptions.assume.Predicate(*args, **kwargs)\n",
    "\n",
    "数学谓词的基类。它还充当未定义谓词对象的构造函数。\n",
    "\n",
    "### 解释\n",
    "\n",
    "Predicate 是返回布尔值[1]的函数。\n",
    "\n",
    "谓词函数是对象，是谓词类的实例。将谓词应用于参数时，将返回 `AppliedPredicate` 实例。这仅仅是包装了参数，并且保持未计算状态。为了获得应用谓词的真值，使用函数 `ask`。\n",
    "\n",
    "谓词的求值是通过多个分派来完成的。您可以将新的处理程序注册到谓词中以支持新的类型。\n",
    "\n",
    "SymPy 中的每个谓词都可以通过 `Q.`的属性访问。例如，`Q.even` 返回一个谓词，用于检查参数是否为偶数。\n",
    "\n",
    "为了定义一个可以计算的谓词，必须定义该类的子类，并创建实例，然后将它注册到 `Q`。最后，根据参数类型分派处理程序。\n",
    "\n",
    "如果使用这个类直接构造谓词，将得到无法调度的 `UndefinedPredicate`。这在构建不需要求值的布尔表达式时非常有用。\n",
    "\n",
    "### 例子\n",
    "\n",
    "应用和计算布尔值:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import Q, ask\n",
    "ask(Q.prime(7))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "可以通过子类化和分派来定义一个新的谓词。在这里，我们定义了一个性感素数的谓词[2]作为一个例子。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import Predicate, Integer\n",
    "class SexyPrimePredicate(Predicate):\n",
    "    name = \"sexyprime\"\n",
    "Q.sexyprime = SexyPrimePredicate()\n",
    "@Q.sexyprime.register(Integer, Integer)\n",
    "def _(int1, int2, assumptions):\n",
    "    args = sorted([int1, int2])\n",
    "    if not all(ask(Q.prime(a), assumptions) for a in args):\n",
    "        return False\n",
    "    return args[1] - args[0] == 6\n",
    "ask(Q.sexyprime(5, 11))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "直接构造返回 `UndefinedPredicate`，它可以应用但不能被调度。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "sympy.assumptions.assume.UndefinedPredicate"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import Predicate, Integer\n",
    "Q.P = Predicate(\"P\")\n",
    "type(Q.P)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle Q.P(1)$"
      ],
      "text/plain": [
       "Q.P(1)"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Q.P(1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "ename": "TypeError",
     "evalue": "<class 'sympy.assumptions.assume.PredicateMeta'> cannot be dispatched.",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mTypeError\u001b[0m                                 Traceback (most recent call last)",
      "\u001b[0;32m<ipython-input-17-9cc711c81391>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mQ\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mP\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mInteger\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;32mlambda\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0massump\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0;32mTrue\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[0;32m/opt/anaconda3/lib/python3.8/site-packages/sympy/assumptions/assume.py\u001b[0m in \u001b[0;36mregister\u001b[0;34m(cls, *types, **kwargs)\u001b[0m\n\u001b[1;32m    331\u001b[0m         \"\"\"\n\u001b[1;32m    332\u001b[0m         \u001b[0;32mif\u001b[0m \u001b[0mcls\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mhandler\u001b[0m \u001b[0;32mis\u001b[0m \u001b[0;32mNone\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 333\u001b[0;31m             \u001b[0;32mraise\u001b[0m \u001b[0mTypeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"%s cannot be dispatched.\"\u001b[0m \u001b[0;34m%\u001b[0m \u001b[0mtype\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mcls\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    334\u001b[0m         \u001b[0;32mreturn\u001b[0m \u001b[0mcls\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mhandler\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0mtypes\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    335\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;31mTypeError\u001b[0m: <class 'sympy.assumptions.assume.PredicateMeta'> cannot be dispatched."
     ]
    }
   ],
   "source": [
    "Q.P.register(Integer)(lambda expr, assump: True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 参考资料\n",
    "\n",
    "R1 https://en.wikipedia.org/wiki/Predicate_(mathematical_logic)\n",
    "\n",
    "R2 https://en.wikipedia.org/wiki/Sexy_prime\n",
    "\n",
    "### 方法 eval(args, assumptions=True)\n",
    "\n",
    "在给定的假设下评估自身(* args)。\n",
    "\n",
    "这只使用直接解析方法，而不使用逻辑推理。\n",
    "\n",
    "handler = <dispatched AskPredicateHandler>\n",
    "\n",
    "### 方法 classmethod register(*types, **kwargs)\n",
    "\n",
    "向处理程序注册签名。\n",
    "\n",
    "### 方法 classmethod register_many(*types, **kwargs)\n",
    "\n",
    "向同一处理程序注册多个签名。\n",
    "\n",
    "## 类 class sympy.assumptions.assume.UndefinedPredicate(name, handlers=None)\n",
    "\n",
    "没有处理程序的谓词。\n",
    "\n",
    "### 解释\n",
    "\n",
    "这个谓词是通过直接使用 `Predicate` 构造而生成的。它没有处理程序，使用参数求值是由 `SAT` 求解器完成的。\n",
    "\n",
    "### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "sympy.assumptions.assume.UndefinedPredicate"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import Predicate, Q\n",
    "Q.P = Predicate('P')\n",
    "Q.P.func"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle P$"
      ],
      "text/plain": [
       "P"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Q.P.name"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 类 sympy.assumptions.assume.assuming (*assumptions)\n",
    "\n",
    "假设的上下文管理器。\n",
    "\n",
    "### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "None\n"
     ]
    }
   ],
   "source": [
    "from sympy.assumptions import assuming, Q, ask\n",
    "from sympy.abc import x, y\n",
    "print(ask(Q.integer(x + y)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "with assuming(Q.integer(x), Q.integer(y)):\n",
    "    print(ask(Q.integer(x + y)))"
   ]
  }
 ],
 "metadata": {
  "interpreter": {
   "hash": "40d3a090f54c6569ab1632332b64b2c03c39dcf918b08424e98f38b5ae0af88f"
  },
  "kernelspec": {
   "display_name": "Python 3.8.8 ('base')",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.8"
  },
  "orig_nbformat": 4
 },
 "nbformat": 4,
 "nbformat_minor": 2
}
